PACKAGE BODY AbsSign IS
   PROCEDURE AbsSign (X: IN OUT Integer) IS
      S: Integer;
   BEGIN
      --#PRE: X = X_anf
      IF X >= 0 THEN
         S := 1;
      ELSE
         X := -X;
         S := -1;
      END IF;
      --#POST: X_anf = S*X AND X >= 0
   END AbsSign;

PROCEDURE test (X: IN OUT Integer) IS
      S: Integer;
   BEGIN
      --#PRE: X >= 0
A := 0;
--#BOUND: B-X
--#INV: (A**2) <= X
WHILE B <= X LOOP
   A := (A+1);
END LOOP;
--#POST: (A**2) <= X AND X < ((A+1)**2)
   END test;
END AbsSign;